$\forall$${\it ds}_{1}$, ${\it ds1'}$, ${\it ds}_{2}$, ${\it ds2'}$:$a$:Id fp$\rightarrow$ Type, ${\it da}$, ${\it da'}$:$a$:Knd fp$\rightarrow$ Type.
\\[0ex]${\it ds}_{1}$ $\subseteq$ ${\it ds1'}$
\\[0ex]$\Rightarrow$ ${\it ds2'}$ $\subseteq$ ${\it ds}_{2}$
\\[0ex]$\Rightarrow$ ${\it da}$ $\subseteq$ ${\it da'}$
\\[0ex]$\Rightarrow$ effect{-}type(${\it ds}_{1}$;${\it ds}_{2}$;${\it da}$) $\subseteq\rho$ effect{-}type(${\it ds1'}$;${\it ds2'}$;${\it da'}$)